(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #xC45C32531F45D5CB) #x000188B864A63E8C))
(constraint (= (f #x5C79692353CDE86E) #x0000B8F2D246A79C))
(constraint (= (f #xC89C94DEA6D1BE0F) #x0001913929BD4DA4))
(constraint (= (f #x4B2C1F8349C6AC68) #x000096583F06938E))
(constraint (= (f #xD5D17DF726E5914C) #x0001ABA2FBEE4DCC))
(constraint (= (f #xEEBC786987211899) #x0BAF1E1A61C84626))
(constraint (= (f #x14D9C361F02E6493) #x053670D87C0B9924))
(constraint (= (f #xE3B5B267FD4D4CF6) #x08ED6C99FF53533D))
(constraint (= (f #x3824904FB2599990) #x0E092413EC966664))
(constraint (= (f #x29365CC868998EB7) #x0A4D97321A2663AD))
(constraint (= (f #x0000000000000000) #x0000000000000002))
(constraint (= (f #xF0A06160A1A43439) #x0E140C2C14348687))
(constraint (= (f #x1E14B069409602D1) #x03C2960D2812C05A))
(constraint (= (f #x52D2824870907853) #x0A5A50490E120F0A))
(constraint (= (f #x4B080205A5A0C097) #x09610040B4B41813))
(constraint (= (f #x24034920E1E00C3D) #x048069241C3C0187))
(constraint (= (f #x5DDFCDEA96A5B81C) #x0777F37AA5A96E07))
(constraint (= (f #xD7862DC089A402DE) #x05E18B70226900B7))
(constraint (= (f #x55E04AE4813E13BA) #x057812B9204F84EE))
(constraint (= (f #xCC4074E6A53AE5D4) #x03101D39A94EB975))
(constraint (= (f #x9CDED14F4416F133) #x0737B453D105BC4C))
(constraint (= (f #xC4265260C195D433) #x010994983065750C))
(constraint (= (f #x7FF15B8229AF4AEF) #x0000FFE2B7045360))
(constraint (= (f #x2BEE5666FE393E41) #x000057DCACCDFC74))
(constraint (= (f #x7815D5165ACA5F31) #x0E05754596B297CC))
(constraint (= (f #xA8F7695DF87CDA8A) #x000151EED2BBF0FA))
(constraint (= (f #x0000000000000000) #x0000000000000002))
(constraint (= (f #x30C0187849428097) #x0618030F09285013))
(constraint (= (f #x816830E0290F083D) #x002D061C0521E107))
(check-synth)
